COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	DECLARE OPCONST bktrkcond 2 [PRE]
C00004 ENDMK
C⊗;
DECLARE OPCONST bktrkcond 2 [PRE];
DECLARE OPCONST newv 1 [PRE];
AXIOM BKTRK_DEF: ∀u v.(bktrkcond (u v) = IF NULL v THEN undef 
ELSE IF match(u, car(newv(car v)))=undef THEN bktrkcond(u, cdr v)
	ELSE IF match(u,car(newv(car v)))*try(mk-subst(cdr(car(cdr(newv(car v)))),
					       match(u, car(newv(car v)))))=undef
		THEN bktrkcond(u, cdr v)
			ELSE cleanup(match(u,car(newv(car v)))*try(
mk-subst(cdr(car(cdr(newv(car v)))), match(u,car(newv (car v))))), u) );;
	


%9∧%6↑n&↓i↓=↓1%2  [
	∀u  (unify(u, arglisti) = subi)  ∧  ∧(¬b%4j%2)   →
 		( ∧(mk-subst(subgoalisti,subi) → (mk-subst(name subi)
							mk-subst(arglisti,subi) ))  ]



AXIOM MATCH_WORKS: ∀u v.(unify(u,v)=match(u,v));;
AXIOM MK-SUBST_WORKS: ∀x u.